a:. ((a) ~ ff)  (a ~ tt) 

latex

ProofTree

Definitions	s ~ t, t  T, s = t, , A, x:AB(x), P  Q, b, x:A. B(x), ff, Type, , b, x:A  B(x), P & Q, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, p  q, p  q, p q, tt, , Unit, left + right
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf